$\forall$$E$:Type, ${\it pred?}$:($E$$\rightarrow$($E$+Unit)), $e$:$E$. first($e$) $\in$ $\mathbb{B}$